es:ES, i, x:Id, ds:x:Id fp Type, k:Knd, T:Type, f:(State(ds)TDeclaredType(ds;x)).
(discrete(i;x))
 @i events of kind k change continuous x to s,v,t. f(s,v) State(ds) (val:T)
 @i events of kind k change x to f State(ds) (val:T) 

latex

Definitions	(x after e), @i(x:T), x. t(x), , t  T, e@i. P(e), P & Q, A c B, @i events of kind k change x to f State(ds) (val:T), P  Q, x:A. B(x), x(s), @i events of kind k change continuous x to f State(ds) (val:T), S  T
Lemmas	top wf, id-deq wf, fpf-cap wf, int inc rationals, event system wf, Id wf, fpf wf, Knd wf, decl-type wf, es-isconst wf, assert wf, decl-state wf, rationals wf, effect p wf, es-E wf, es-loc wf, es-kind wf